$\forall$$a$:Atom1, $A$:MsgA, $k$:Knd.
\\[0ex]AtomFree(ds($A$))
\\[0ex]$\Rightarrow$ AtomFree(da($A$))
\\[0ex]$\Rightarrow$ $\lambda$$z$,${\it z@}_{0}$,$x$. $A$.ef($k$,$x$,${\it z@}_{0}$,$z$)?${\it z@}_{0}$($x$):$A$.da($k$)$\rightarrow$$A$.state$\rightarrow$$A$.state$>>$$a$
\\[0ex]$\Rightarrow$ ma{-}body($A$):Shape($A$)$>>$$a$